;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Itranspose-fast.lisp")

(module Mtranspose-fast

  (defun transpose-fast-aux (matrix)
    (if (endp matrix)
        (mv nil nil)
        (let ((element-to-append (caar matrix))
              (new-row (cdar matrix)))
          (mv-let (acc new-row-list)
                  (transpose-fast-aux (cdr matrix))
                  (mv (cons element-to-append acc)
                      (cons new-row new-row-list))))))
  
  (defun transpose-fast (matrix)
    (if (endp (car matrix))
        nil
        (mv-let (new-row remaining-matrix)
                (transpose-fast-aux matrix)
                (cons new-row
                      (transpose-fast remaining-matrix)))))

  (export Itranspose-fast))

